the_w:World, l:IdLnk, e:E. sends(l;e)  Msg_sub(l;the_w.M) List 

latex

Definitions	haslink(l;m), onlnk(l;mss), Msg_sub(l;M), World, t  T, IdLnk, x:A. B(x), E, sends(l;e), mlnk(m), source(l), Id, time(e), loc(e), m(i;t), P  Q, w.M, Msg(M), type List, S  T, a = b, x.A(x), f(a), b, {x:A| B(x) }, P & Q, P  Q
Lemmas	assert-eq-lnk, subtype rel list, assert wf, filter type, eq lnk wf, w-m wf, w-loc wf, w-time wf, Msg wf, w-M wf, Id wf, lsrc wf, mlnk wf, w-E wf, IdLnk wf, world wf